$\forall$$M$:MsgA, $k$:Knd, $s$:$M$.state, $v$:$M$.da($k$), $x$:Id, $w$:$M$.ds($x$). $M$.ef($k$,$x$,$s$,$v$,$w$) $\in$ Prop